s:LOSet, a, b:|s|. ((a  b))  (b <s a) 

latex

Up	sets 1
Definitions of Statement	PosetSig, DSet, QOSet, POSet{i}, LOSet
Definitions	t  T, x:A. B(x), P & Q, x,y. t(x;y), P  Q, P  Q, P  Q, Order(T;x,y.R(x;y)), Linorder(T;x,y.R(x;y)), DSet, QOSet, POSet{i}, LOSet, x(s1,s2), , Preorder(T;x,y.R(x;y))
Lemmas	loset wf, set car wf, set lt is sp of leq, strict part wf, set lt wf, set leq wf, not wf, iff functionality wrt iff, linorder le neg, set eq wf, eqfun p wf, poset sig wf, dset properties, preorder wf, dset wf, qoset properties, anti sym wf, qoset wf, poset properties, connex wf, poset wf, loset properties